es:ES, ds:x:Id fp Type, T:Type, i:Id, f:(State(ds)T).
(x, y:T. Dec(x = y))
 (x:Id. vartype(i;x)  ds(x)?Top)
 e'@i.
 (e:E. e  e'   f((state when e)) = f(state after e')  T)
  (e:E.
  (e  e' 
  (& f((state when e)) = f(state after e')
  (& & (e'':E. (e <loc e'')  e''  e'   f((state when e'')) = f(state after e')  T)) 

latex

Definitions

x:A. B(x), State(ds), P  Q, e@i. P(e), P  Q, x:A. B(x), A & B, P & Q, Prop, t  T, x. t(x), state@i, {T}, T, True, e  e' , SQType(T), A, (e <loc e'), P  Q, x(s), P  Q, Dec(P), False, Trans x,y:T. E(x;y)

Lemmas

alle-at-iff, es-state-when wf, subtype rel dep function, es-vartype wf, es-loc wf, fpf-cap wf, id-deq wf, top wf, subtype rel self, es-le-loc, es-state-after wf, not wf, es-loc-pred, es-locl-iff, assert wf, es-first wf, Id wf, decidable wf, decl-state wf, fpf wf, event system wf, es-le wf, es-le-iff, squash wf, true wf, es-E wf, es-le-self, es-locl wf, es-locl-antireflexive, es-pred wf, state-after-pred, equal functionality wrt subtype rel, es-state wf, Id sq, es-locl-trans